change-to(x;e)
== case TERMOF{change-to-lemma2:ObjectId, i:l, i:l}(T,eq,es,x,e)
== of inl(p) => inl (p.1) 
== o| inr(q) => inr   

latex

---

clarification:

change-to{i:l}
change-to(T; eq; es; x; e)
== case TERMOF{change-to-lemma2:ObjectId, i:l, i:l}(T,eq,es,x,e)
== of inl(p) => inl (p.1) 
== o| inr(q) => inr   

latex

Definitions	case b of inl(x) => s(x) | inr(y) => t(y), f(a), change-to-lemma2, inl x , t.1, inr x ,
FDL editor aliases	change-to